Nuprl Definition : comp-atom-ap 11,40

comp-atom-ap(gfxa)
== let f' = a.compose(gf) in
== let f'let x' = a.x in
== let f'let x'let F = b,cf'(b,x'(c)) in
== let f'let x'let Flet L = atoms-in(F) in
== let f'let x'let Flet Llet b = new-atom(cons(aL)) in
== let f'let x'let Flet Llet bif eq_atom((F(b,a)); a)
== let f'let x'let Flet Llet bifthen inr (f'(b)) 
== let f'let x'let Flet Llet if eq_atom((F(a,b)); a)
== let f'let x'let Flet Llet ifthen inl (f.g(f(x'(b)))) 
== let f'let x'let Flet Llet else inr (x.hd(list-diff(atom-deq; monitor((f'(b,x))); cons(bL)))) 
== let f'let x'let Flet Llet fi  
latex


Definitionscompose(fg), let x = a in b(x), if b then t else f fi , eq_atom(xy), inl x , inr x , x.A(x), hd(l), list-diff(eqasbs), atom-deq, f(a), cons(carcdr)
FDL editor aliasescomp-atom-ap

origin